Inference at * 1 
Iof proof for Lemma multiply functionality wrt le:



1. i1 : 
2. i2 : 
3. j1 : 
4. j2 : 
5. i1  j1
6. i2  j2
  (i1 * i2)  (j1 * j2) 

latex

 by ((Using [`n',i1] (FwdThruLemma `mul_preserves_le` [6])) 
CollapseTHENA ((Auto_aux (first_nat 
C1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 7. (i1 * i2)  (i1 * j2)
C1:   (i1 * i2)  (j1 * j2)
C.

Definitions	t  T, P  Q, x:A. B(x),
Lemmas	mul preserves le